package sketch.specs;

import java.util.LinkedList;
import java.util.List;

import sketch.ounit.Observer;
import sketch.ounit.Values;
import sketch.specs.annotation.TestSketch;
import junit.framework.TestCase;

public class SketchExampleWithAuxiliaryMethods extends TestCase {
	
	
	@TestSketch
	public void testExample() {
		List<Integer> list = new LinkedList<Integer>();
		list.add(10);
		{/*@ChooseOne*/
			list.clear();
			list.add(20);
		}
		Observer.observeExpr(list);
		
		int r1 = auxiliary1(Values.symbolicInt());
		int r2 = auxiliary2(r1);
		System.out.println(r2);
	}
	
	public int auxiliary1(int x) {
		if( x> 10) {
			return 100;
		} else if ( x< 9) {
			return x*10;
		} else {
			return x + 3;
		}
	}
	
	public int auxiliary2(int x) {
		if(x == 12 || x == 13) {
			return 16;
		} else if ( x < 0 ) {
			return 0;
		} else {
			return x * 7 + 9;
		}
	}
	
}
